T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} ,
v:T. (x changed before e)  (es-when(es; x; e) = v)  @(last change to x before e)(xv) 

latex

Definitions	t  T, x:A. B(x), loc(e), es-dtype(es; i; x; T), es-E(es), {x:A| B(x)} , x:AB(x), b, s = t, @e(xv), P  Q, Id, event_system{i:l}, EqDecider(T), Type, (last change to x before e), prop{i:l}, sqequal(s; t), guard(T), sq_type(T), x changed before e, es-vartype(es; i; x), x:A  B(x), P  Q, es-when(es; x; e), atom{$n:n}, if b then t else f fi , A c B
Lemmas	es-when wf, es-vartype wf, subtype rel self, assert wf, changed wf, es-change-to wf, last-change wf, last-change-property, deq wf, event system wf, Id wf, es-E wf, es-dtype wf, es-loc wf